COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 unify.lsp[s84,jmc]	Unification algorithm
C00004 ENDMK
C⊗;
;;; unify.lsp[s84,jmc]	Unification algorithm

;;; This unify assumes that  e1  and  e2  have no variables in common.
(defun unify (e1 e2 a)
       (cond
	((eq a 'no) 'no)
	((isconst e1)
	 (if (isconst e2)
	     (if (equal e1 e2) a 'no)
	     (unify e2 e1 a)))
	((isvar e1)
	 (let ((e1a (assoc e1 a)))
	      (if
	       (null e1a)
	       (cons (cons e1 e2) a)
	       (unify (cdr e1a) e2 a))))
	((isconst e2) 'no)
	((isvar e2)
	 (unify e2 e1 a))
	(t (unify (cdr e1) (cdr e2) (unify (car e1) (car e2) a)))))

(defun isvar (e) (memq e '(x x0 x1 x2 y y0 y1 y2 z z0 z1 z2)))

(defun isconst (e)
       (if (atom e)
	   (not (isvar e))
	   (eq (car e) 'quote)
))

(unify 'a 'b nil)

(unify 'x 'a nil)

(unify 'x 'y nil)

(unify '(f a) '(g a) nil)

(unify '(f a) '(f a) nil)

(unify '(f x) '(f a) nil)

(unify '(f x (g a)) '(f (h b) y) nil)

(unify 'x 'y '((x.a)))
((Y . A) (X . A)) 

(unify 'y 'x '((x.a)))
((Y . X) (X . A))